$\forall$$T$, ${\it T'}$:Type, $E$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), ${\it E'}$:(${\it T'}$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$).
\\[0ex]($T$ = ${\it T'}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. $E$($x$,$y$) $\Leftarrow\!\Rightarrow$ ${\it E'}$($x$,$y$))
\\[0ex]$\Rightarrow$ (EquivRel($T$;$x$,$y$.$E$($x$,$y$)) $\Leftarrow\!\Rightarrow$ EquivRel(${\it T'}$;$x$,$y$.${\it E'}$($x$,$y$)))